////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009 The Mist project                                        //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the implementation of the KeY Solver.
///

#include "keysolver.hpp"

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include <fstream>
using std::ifstream;
using std::ofstream;

#include <boost/filesystem.hpp>
namespace bf = ::boost::filesystem;

#include <boost/process.hpp>
namespace bp = ::boost::process;

#include <boost/regex.hpp>

#include "common/assert.hpp"
#include "common/string.hpp"
#include "keyinput.hpp"

////////////////////////////////////////////////////////////////////////////////
// Static Constant Initializations                                            //
////////////////////////////////////////////////////////////////////////////////

const string KeySolver::PathToKey = "./KeY/bin/startProver";
const uint   KeySolver::TimeOut   = 100000;

////////////////////////////////////////////////////////////////////////////////
// Function Implementations                                                   //
////////////////////////////////////////////////////////////////////////////////

KeySolver::KeySolver(sptr<Expression> problem) : _problem(problem) {
	assert(problem);
	
	// Generate a unique filename.
	//
	_problemFile = _tempFileName();
	
	// Create new file containing the key formula we try to prove.
	//
	ofstream keyProblemFile((_problemFile + ".key").c_str());
	// TODO: checken of bestand maken gelukt is
	keyProblemFile << KeyInput(problem);
	keyProblemFile.close();
	_keyStatus = NOT_STARTED;
}

wptr<Expression> KeySolver::problem() const {
	return _problem;
}

void KeySolver::start_key() {
	::boost::process::command_line cl(PathToKey);
	cl.argument("auto");
	cl.argument("timeout " + to_string(TimeOut));
	cl.argument(_problemFile + ".key");
	
	::boost::process::launcher l;
	
	_process = new ::boost::process::child(l.start(cl));
	_keyStatus = BUSY;
}

string KeySolver::report() {
	_setProofStatus();
	
	assert(proof_status() != FAILED);
	
	// TODO: checken of bestand bestaat
	ifstream keyProofFile((_problemFile + ".auto.0.proof").c_str());
	
	string result, line;
	while(getline(keyProofFile, line))
		result += line + "\n";
	
	return result;
}

string KeySolver::proof_file() {
	_setProofStatus();
	assert(proof_status() != FAILED);
	
	return _problemFile + ".auto.0.proof";
}

KeySolver::ProofStatus KeySolver::proof_status() {
	_setProofStatus();
	return _proofStatus;
}

string KeySolver::_tempFileName() {
	uint i;
	for (i = 0; bf::exists("/tmp/key" + to_string(i) + ".key"); ++i);
	return "/tmp/key" + to_string(i);
}

void KeySolver::_setProofStatus() {
	if(_keyStatus == NOT_STARTED)
		start_key();
	if(_keyStatus == BUSY) {
		::boost::process::status s = _process->wait();
		_keyStatus = FINISHED;
		
		if (s.exited() && s.exit_status() == 0) {
			_proofStatus = PROVED;
		} else if (s.exited() && s.exit_status() == 1) {
			_proofStatus = NOT_PROVED;
			
			string haystack = report();
			string needle   = "(autoModeTime \"";
			size_t pos = haystack.find(needle, 0);
			
			if (pos != string::npos) {
				string autoModeTime;
				pos += needle.size();
				while (haystack[pos] != '"')
					autoModeTime += haystack[pos++];
				if (to<uint>(autoModeTime) >= TimeOut)
					_proofStatus = TIMEOUT;
			}
		} else {
			_proofStatus = FAILED;
		}
	}
}
